#include "learner.h"
#include "translator.h"
#include <iostream>
using namespace cdnf;
Learner::Learner(Teacher* teacher, int numberOfVar):teacher(teacher),numberOfVar(numberOfVar),t(-1){}
CDNF& Learner::learn(){
	if (teacher->isEqual(candidate)) 
		return candidate;
	addUnit(teacher->getCounterexample());
	learnCDNF();
	return candidate;
}
void Learner::learnCDNF(){
	while (!teacher->isEqual(candidate)) {
		//counterExample = teacher->getCounterexample();
		if(teacher->failed){
			return;
		}
		if(teacher->flag){
			learnByPartial(teacher->cterms);
			continue;
		}
		std::vector<int> indexList;		
		std::vector<DNF> dnfs = candidate.getDnfs();

		
		for (int i = 0; i <= t; i++) {		
			if (!dnfs[i].getValue(teacher->getCounterexample()))
				indexList.push_back(i);
		}
		if (indexList.size() == 0) {
			addUnit(teacher->getCounterexample());			

		} else {
			for (unsigned int i=0;i<indexList.size();i++) {
				int index=indexList[i];
				Valuation u = teacher->getCounterexample();
				
				walkTowardsA(u, units[index].a);
				
				(units[index].S).push_back(u.xorValuation(units[index].a));
			}
			constructDNFs();
		}
		//printCDNF(candidate);
		logMessage("end learn");
	}
		

}
void Learner::learnByPartial(std::vector<int> terms){
	std::vector<int> indexList;
	std::vector<DNF> dnfs = candidate.getDnfs();
	for (int i = 0; i <= t; i++) {		
		if (!dnfs[i].getValue(terms))
			indexList.push_back(i);
	}
	assert(indexList.size()>0);
	for (unsigned int i=0;i<indexList.size();i++) {
		int index=indexList[i];
		Valuation u;
		u.clone(units[index].a);
		for(int i=0;i<terms.size();i++){
			int index = abs(terms[i]);
			u.set(index,(terms[i]>0));
		}
		assert(!dnfs[index].getValue(u));
		walkTowardsA(u, units[index].a);
		
		(units[index].S).push_back(u.xorValuation(units[index].a));
	}
	constructDNFs();

}
void Learner::restart(){}
CDNF& Learner::getCandidate(){
	return this->candidate;
}
//鍒╃敤ai鍜孲i鏋勯�鐩稿簲鐨凞NF
void Learner::constructDNFs(){
	for (int i = 0; i <= t; i++) {
		Valuation a = units[i].a;
		DNF dnf;

		// if Si is empty, DNFi=False
		if (units[i].S.size() == 0) {
			dnf.setDegeneratedValue(false);
			candidate.setDNF(i, dnf);
			continue;
		}

		for (unsigned int k=0;k<units[i].S.size();k++) {
			Valuation s=units[i].S[k];
			Conjunction c;
			for (int j = 1; j <= numberOfVar; j++) {
				if (s[j]) {
					if (a[j])
						c.addTerm(-j);
					else
						c.addTerm(j);
				}
			}
			
			if (c.getTerms().size() == 0)
				c.setDegeneratedValue(true);
			dnf.addConjunction(c);
		}
		candidate.setDNF(i, dnf);
	}
}
Valuation Learner::walkTowardsA(Valuation& u, Valuation& a){
	int i = 1;
	
	while (i <= numberOfVar) {
		if (u[i] != a[i]) {
			u.set(i,!u[i]);						
			if (teacher->isMembership(u)) {
				i = 0;
			} else {
				u.set(i,!u[i]);
			}
		}
		i++;
	}
	bool check = true;
        for (i = numberOfVar; check && i > 0; i--) {
	       if (u[i] != a[i]) check = false;
        }
        assert (!check);

	return u;
}

void Learner::addUnit(Valuation& counterExample){
	logMessage("add unit");
	t++;
	DNF dnf;
	candidate.addDNF(dnf);
	unit u;
	for(int i=1;i<=numberOfVar;i++)
		u.a.add(counterExample[i]);
	units.push_back(u);
}

